00100	PRE_PRED: R,A,B;
00200	INF_PRED:=; EQUALITY:=;
00300	VAR: W,X,Y,Z,X1,X2;
00400	F1: ∀(X,Y)∃Z R(X,Y,Z);
00500	F2: ∀(W,X,Y,Z)( R(X,Y,Z) ∧ R(X,Y,W) ⊃ W=Z );
00600	F3: ∀(X1,X2)∃X∀(Y,Z,W)( R(X1,Y,W) ∧ R(X2,W,Z) ⊃ R(X,Y,Z) );
00700	A1:  ∃(X,W)( A(W) ∧ ∀(Y,Z)( B(Y) ∧ R(X,Y,Z) ⊃ A(Z) ∧ ¬W=Z ));
00800	A2: ¬∃(X,W)( A(W) ∧ ∀(Y,Z)( A(Y) ∧ R(X,Y,Z) ⊃ A(Z) ∧ ¬W=Z ));
00900	THM: ¬∃X∀(Y,Z)( A(Y) ∧ R(X,Y,Z) ⊃ B(Z) );
01000	;
01100